/* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files
 * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify,
 * merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
 * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF
 * OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 */

package edu.mit.csail.sdg.alloy4compiler.ast;

import java.util.ArrayList;
import java.util.Collection;
import java.util.List;
import edu.mit.csail.sdg.alloy4.Pos;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.ErrorWarning;
import static edu.mit.csail.sdg.alloy4compiler.ast.Sig.UNIV;

/** Immutable; represents a constant in the AST. */

public final class ExprConstant extends Expr {

    /** The type of constant. */
    public final Op op;

    /** If this node is a String constant, then this field stores the String, else this field stores "". */
    public final String string;

    /** If this node is a number constant, then this field stores the number, else this field stores 0. */
    public final int num;

    /** Return the number if this node is a number constant, otherwise return 0. */
    public int num() { return num; }

    /** {@inheritDoc} */
    @Override public Pos span() { return pos; }

    /** {@inheritDoc} */
    @Override public void toString(StringBuilder out, int indent) {
        if (indent<0) {
            if (op==Op.NUMBER) out.append(num); else if (op==Op.STRING) out.append(string); else out.append(op);
        } else {
            for(int i=0; i<indent; i++) { out.append(' '); }
            if (op==Op.NUMBER) out.append(num); else if (op==Op.STRING) out.append(string); else out.append(op);
            out.append('\n');
        }
    }

    /** Constructs an ExprConstant node.
     *
     * @param pos - the original position in the file
     * @param op - the choice of which constant it is
     * @param num - the number (this argument is ignored if op!=NUMBER)
     */
    private ExprConstant(Pos pos, Op op, int num, String string) {
        super(pos, null, false,
            (op==Op.IDEN ? Type.make2(UNIV) :
                (op==Op.NEXT ? Type.make2(Sig.SIGINT) :
                    (op==Op.TRUE || op==Op.FALSE ? Type.FORMULA :
                        (op==Op.EMPTYNESS ? UNIV.type : (op==Op.STRING ? Sig.STRING.type : Type.INT))))), 0, 0, null);
        this.op = op;
        this.num = (op==Op.NUMBER ? num : 0);
        this.string = (op==Op.STRING ? string : "");
    }

    /** Returns true if we can determine the two expressions are equivalent; may sometimes return false. */
    @Override public boolean isSame(Expr obj) {
        while(obj instanceof ExprUnary && ((ExprUnary)obj).op==ExprUnary.Op.NOOP) obj=((ExprUnary)obj).sub;
        if (obj==this) return true;
        if (!(obj instanceof ExprConstant)) return false;
        ExprConstant x=(ExprConstant)obj;
        if (op==Op.STRING) return op==x.op && string.equals(x.string); else return op==x.op && num==x.num;
    }

    /** The "TRUE" boolean value. */
    public static final Expr TRUE = new ExprConstant(null, Op.TRUE, 0, "");

    /** The "FALSE" boolean value. */
    public static final Expr FALSE = new ExprConstant(null, Op.FALSE, 0, "");

    /** The "iden" relation. */
    public static final Expr IDEN = new ExprConstant(null, Op.IDEN, 0, "");

    /** The smallest integer value allowed by the current bitwidth. */
    public static final Expr MIN = new ExprConstant(null, Op.MIN, 0, "");

    /** The largest integer value allowed by the current bitwidth. */
    public static final Expr MAX = new ExprConstant(null, Op.MAX, 0, "");

    /** The "next" relation relating each integer to its next larger integer. */
    public static final Expr NEXT = new ExprConstant(null, Op.NEXT, 0, "");

    /** The "0" integer. */
    public static final Expr ZERO = new ExprConstant(null, Op.NUMBER, 0, "");

    /** The "1" integer. */
    public static final Expr ONE = new ExprConstant(null, Op.NUMBER, 1, "");

    /** The "emptyness" constant. */
    public static final Expr EMPTYNESS = new ExprConstant(null, Op.EMPTYNESS, 0, "");

    /** Constructs the integer "n" */
    public static Expr makeNUMBER(int n) {
        if (n==0) return ZERO;
        if (n==1) return ONE;
        return new ExprConstant(null, Op.NUMBER, n, "");
    }

    /** This class contains all possible constant types. */
    public enum Op {
        /** true                                      */  TRUE("true"),
        /** false                                     */  FALSE("false"),
        /** the builtin "iden" relation               */  IDEN("iden"),
        /** the minimum integer constant              */  MIN("min"),
        /** the maximum integer constant              */  MAX("max"),
        /** the "next" relation between integers      */  NEXT("next"),
        /** the emptyness relation whose type is UNIV */  EMPTYNESS("none"),
        /** a String constant                         */  STRING("STRING"),
        /** an integer constant                       */  NUMBER("NUMBER");

        /** The constructor. */
        private Op(String label) {this.label=label;}

        /** The human readable label for this operator. */
        private final String label;

        /** Makes an ExprConstant node
         * @param pos - the original position in the source file (can be null if unknown)
         * @param number - the number (this argument is ignored if op!=NUMBER)
         */
        public final ExprConstant make(Pos pos, int number) { return new ExprConstant(pos, this, number, ""); }

        /** Makes an ExprConstant node
         * @param pos - the original position in the source file (can be null if unknown)
         * @param string - the string (this argument is ignored if op!=STRING)
         */
        public final ExprConstant make(Pos pos, String string) { return new ExprConstant(pos, this, 0, string); }

        /** Returns the human readable label for this operator. */
        @Override public final String toString() { return label; }
    }

    /** {@inheritDoc} */
    @Override public Expr resolve(Type type, Collection<ErrorWarning> warns) { return this; }

    /** {@inheritDoc} */
    @Override final<T> T accept(VisitReturn<T> visitor) throws Err { return visitor.visit(this); }

    /** {@inheritDoc} */
    public int getDepth() { return 1; }

    /** {@inheritDoc} */
    @Override public String getDescription() {
        switch(op) {
          case TRUE: return "<b>true</b>";
          case FALSE: return "<b>false</b>";
          case IDEN: return "<b>iden</b>";
          case MAX: return "<b>fun/max</b>";
          case MIN: return "<b>fun/min</b>";
          case NEXT: return "<b>fun/next</b>";
          case EMPTYNESS: return "<b>none</b>";
          case STRING: return "<b>\"" + string + "\"</b>";
        }
        return "<b>" + num + "</b>";
    }

    /** {@inheritDoc} */
    @Override public List<? extends Browsable> getSubnodes() { return new ArrayList<Browsable>(0); }
}
